<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
  <head>
    <title>package alloy.sharbool</title>
  </head>

  <body>
    Ensures that identical Boolean subformulas are shared
    in the Boolean DAG to which the Alloy formula is translated.  You don't need to understand this package
    unless you're changing how Alloy's translation to Boolean formulas works.

    The sharing covers simple cases e.g. when an identical subformula such as "A in B.C" occurs in two different
    places in the Alloy model (where A, B and C are relations), but also more subtle cases -- e.g. in the subformulas
    "all s: State | T(F(s), F(s.next))" which denotes "T(F(s0),F(s1)) && T(F(s1),F(s2)) && ..." it will ensure that
    the translations of the two copies of "F(s1)" are shared in the Boolean DAG.
    <hr>
    <address><a href="mailto:Administrator@TYNDA"></a></address>
<!-- Created: Mon Apr 04 12:15:06 Eastern Daylight Time 2005 -->
<!-- hhmts start -->
Last modified: Mon Apr 04 12:20:00 Eastern Daylight Time 2005
<!-- hhmts end -->
  </body>
</html>
